Nuprl Lemma : l_member_set 11,40
A:Type, P:(Aprop{i:l}), L:(A List), x:A. l_all(L; A; x.P(x))  guard(((x  L)  (x  L))) 
latex

Definitionsx(s), guard(T), x. t(x), l_all(L; T; x.P(x)), (x  l), x:A. B(x), l[i], ge(i; j), A c B, subtype(S; T), x:A. B(x), , A  B, A, False, P  Q, ||as||, t  T, prop{i:l}
Lemmaslist-set-type2, select wf, length wf1, l all wf, l member wf

origin